COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	CS258		MATHEMATICAL THEORY OF COMPUTATION      WINTER 1975
C00008 ENDMK
C⊗;
CS258		MATHEMATICAL THEORY OF COMPUTATION      WINTER 1975


        AN EXAMPLE OF MANNA'S METHOD

	Consider the program

	I ← N;
	K  ← 0;
LOOP:	if I=0 then go to DONE;
	I ← I-1;
	K  ← K+M;
	go to LOOP;
DONE:

	We would like to prove by Manna's method that the program terminates
for all non-negative values of M and N, and when it terminates we have.

1)	K = M*N.

	Manna's method is a kind of dual to Floyd's inductive assertion
method for proving partial correctness.  Let us review the application
of the inductive assertion method to proving this program partially
correct.  All we have to do is attach a suitable predicate to the statement
labelled LOOP, and the right predicate is

2)	K = M*(N-I).

We first note that the predicate is initially true, because initially 
I=N and K=0.  Next we note that if I is not zero so that we go around
the loop, at the next time we reach LOOP, the new values of I and K (
namely I and K+M) again satisfy 2); this follows from the predicate
calculus sentence

3)	∀I K.(K=M*(N-I) ⊃ K+M=M*(N-(I-1))

which the reader might try to prove as an exercise in using the proof
checker.  Finally, we note that if I=0, then we go to DONE, and the
desired condition 1) follows from 2) and the fact that I=0.
Of course, this gives us only partial correctness, i.e. we know that
if the program terminates, then K has the right value.

	To go from here to Manna's method, we imagine that someone
wished to prove the program "partially incorrect", i.e. he wishes
to prove that either the program doesn't terminate, or if it does
terminate, then K≠M*N.  If he wished to do this by the inductive
assertion method, he would have to invent a predicate Q(I,K) that
would play the role of 2) in his proof.  He would have to prove that
Q(I,K) is initially satisfied (i.e. Q(N,0))
and also that if I≠0, then the condition
is again satisfied after going arount the loop, i.e. he would have to
prove

4)	∀I K.(I≠0 ∧ Q(I,K) ⊃ Q(I-1,K+M).

All this is just as in proving partial correctness, but his task in the
termination case is different; he would have to prove

5)	I=0 ∧ Q(I,K) ⊃ K≠M*N.

Putting all this together, he would have to find a predicate Q(I,K)
for which he could prove

6) Q(N,0) ∧ ∀I K.((Q(I,K)∧I≠0 ⊃ Q(I-1,K+M)) ∧ (Q(I,K)∧I=0 ⊃ K≠M*N)).

Using conditional expressions allows 6) to be written more neatly as

7) Q(N,0) ∧ ∀I K.(Q(I,K) ⊃ (if I=0 then K≠M*N else Q(I-1,K+M))).

Manna's method for proving the program correct simply consists in showing
that it is impossible to prove it incorrect as outlined above.  To do this
we have but to prove the negation of 6) or 7) for all predicates Q.  Thus we
must prove

8) ∀N(¬Q(N,0)∨Q(0,M*N)∨¬∀I K.(I≠0 ∧ Q(I,K) ⊃ Q(PRED I,K+M))).

(In going from 6) to 8), we attached the negation sign and put a universal
quantifier in front.  Besides that, we took the case I=0 out of the inner
quantifier and wrote PRED I instead of I-1.

	If we can prove 8), we will show that no-one can prove the program
incorrect.  On the face of it, this doesn't prove the program correct, but
this logical gap is easily remedied.  Namely, we have only to remark that if
the program were incorrect, a suitable Q(I,K) could be obtained by making
it true for exactly those pairs (I,K) that occurred in an incorrect run of
the program.

	In proving 8), the predicate symbol Q is taken as free; we must
prove 8) for arbitrary Q.  On the other hand, we must assume that the
constant functions for addition and multiplication and predecessor have
the standard interpretations of arithmetic.

	Attached to this writeup is an FOL proof of 8) from the axioms
INTEGE.AX together with a few arithmetic theorems called ADHOC.THE which
are left as exercises for the reader to prove in FOL.